0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 12 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 10 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 27 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
PERM_IN_GA(L, .(H, T)) → U1_GA(L, H, T, append2_in_aag(V, .(H, U), L))
PERM_IN_GA(L, .(H, T)) → APPEND2_IN_AAG(V, .(H, U), L)
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → U5_AAG(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → APPEND2_IN_AAG(L1, L2, L3)
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_GA(L, H, T, append1_in_gga(V, U, W))
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → APPEND1_IN_GGA(V, U, W)
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → U4_GGA(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → APPEND1_IN_GGA(L1, L2, L3)
U2_GA(L, H, T, append1_out_gga(V, U, W)) → U3_GA(L, H, T, perm_in_ga(W, T))
U2_GA(L, H, T, append1_out_gga(V, U, W)) → PERM_IN_GA(W, T)
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
PERM_IN_GA(L, .(H, T)) → U1_GA(L, H, T, append2_in_aag(V, .(H, U), L))
PERM_IN_GA(L, .(H, T)) → APPEND2_IN_AAG(V, .(H, U), L)
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → U5_AAG(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → APPEND2_IN_AAG(L1, L2, L3)
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_GA(L, H, T, append1_in_gga(V, U, W))
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → APPEND1_IN_GGA(V, U, W)
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → U4_GGA(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → APPEND1_IN_GGA(L1, L2, L3)
U2_GA(L, H, T, append1_out_gga(V, U, W)) → U3_GA(L, H, T, perm_in_ga(W, T))
U2_GA(L, H, T, append1_out_gga(V, U, W)) → PERM_IN_GA(W, T)
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → APPEND1_IN_GGA(L1, L2, L3)
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
APPEND1_IN_GGA(.(H, L1), L2, .(H, L3)) → APPEND1_IN_GGA(L1, L2, L3)
APPEND1_IN_GGA(.(L1), L2) → APPEND1_IN_GGA(L1, L2)
From the DPs we obtained the following set of size-change graphs:
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → APPEND2_IN_AAG(L1, L2, L3)
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
APPEND2_IN_AAG(.(H, L1), L2, .(H, L3)) → APPEND2_IN_AAG(L1, L2, L3)
APPEND2_IN_AAG(.(L3)) → APPEND2_IN_AAG(L3)
From the DPs we obtained the following set of size-change graphs:
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_GA(L, H, T, append1_in_gga(V, U, W))
U2_GA(L, H, T, append1_out_gga(V, U, W)) → PERM_IN_GA(W, T)
PERM_IN_GA(L, .(H, T)) → U1_GA(L, H, T, append2_in_aag(V, .(H, U), L))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(L, .(H, T)) → U1_ga(L, H, T, append2_in_aag(V, .(H, U), L))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_ga(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_ga(L, H, T, append1_in_gga(V, U, W))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U2_ga(L, H, T, append1_out_gga(V, U, W)) → U3_ga(L, H, T, perm_in_ga(W, T))
U3_ga(L, H, T, perm_out_ga(W, T)) → perm_out_ga(L, .(H, T))
U1_GA(L, H, T, append2_out_aag(V, .(H, U), L)) → U2_GA(L, H, T, append1_in_gga(V, U, W))
U2_GA(L, H, T, append1_out_gga(V, U, W)) → PERM_IN_GA(W, T)
PERM_IN_GA(L, .(H, T)) → U1_GA(L, H, T, append2_in_aag(V, .(H, U), L))
append1_in_gga([], L, L) → append1_out_gga([], L, L)
append1_in_gga(.(H, L1), L2, .(H, L3)) → U4_gga(H, L1, L2, L3, append1_in_gga(L1, L2, L3))
append2_in_aag([], L, L) → append2_out_aag([], L, L)
append2_in_aag(.(H, L1), L2, .(H, L3)) → U5_aag(H, L1, L2, L3, append2_in_aag(L1, L2, L3))
U4_gga(H, L1, L2, L3, append1_out_gga(L1, L2, L3)) → append1_out_gga(.(H, L1), L2, .(H, L3))
U5_aag(H, L1, L2, L3, append2_out_aag(L1, L2, L3)) → append2_out_aag(.(H, L1), L2, .(H, L3))
U1_GA(append2_out_aag(V, .(U))) → U2_GA(append1_in_gga(V, U))
U2_GA(append1_out_gga(W)) → PERM_IN_GA(W)
PERM_IN_GA(L) → U1_GA(append2_in_aag(L))
append1_in_gga([], L) → append1_out_gga(L)
append1_in_gga(.(L1), L2) → U4_gga(append1_in_gga(L1, L2))
append2_in_aag(L) → append2_out_aag([], L)
append2_in_aag(.(L3)) → U5_aag(append2_in_aag(L3))
U4_gga(append1_out_gga(L3)) → append1_out_gga(.(L3))
U5_aag(append2_out_aag(L1, L2)) → append2_out_aag(.(L1), L2)
append1_in_gga(x0, x1)
append2_in_aag(x0)
U4_gga(x0)
U5_aag(x0)
U1_GA(append2_out_aag(V, .(U))) → U2_GA(append1_in_gga(V, U))
U2_GA(append1_out_gga(W)) → PERM_IN_GA(W)
PERM_IN_GA(L) → U1_GA(append2_in_aag(L))
append1_in_gga([], L) → append1_out_gga(L)
append1_in_gga(.(L1), L2) → U4_gga(append1_in_gga(L1, L2))
append2_in_aag(L) → append2_out_aag([], L)
append2_in_aag(.(L3)) → U5_aag(append2_in_aag(L3))
U4_gga(append1_out_gga(L3)) → append1_out_gga(.(L3))
U5_aag(append2_out_aag(L1, L2)) → append2_out_aag(.(L1), L2)
append1ingga2 > [] > PERMINGA1 > .1 > U2GA1 > append2inaag1 > U1GA1 > U5aag1 > append2outaag2 > U4gga1 > append1outgga1
[]=2
append1_out_gga_1=6
._1=7
U4_gga_1=7
append2_in_aag_1=2
U5_aag_1=7
U1_GA_1=3
U2_GA_1=1
PERM_IN_GA_1=6
append1_in_gga_2=8
append2_out_aag_2=0
append1_in_gga(x0, x1)
append2_in_aag(x0)
U4_gga(x0)
U5_aag(x0)